(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-sort tptp.list 0)
(declare-fun tptp.nil () tptp.list)
(declare-fun tptp.mycons (Int tptp.list) tptp.list)
(declare-fun tptp.fib_sorted (tptp.list) Bool)
(assert (tptp.fib_sorted tptp.nil))
(assert (forall ((X Int)) (tptp.fib_sorted (tptp.mycons X tptp.nil))))
(assert (forall ((X Int) (Y Int)) (=> (< X Y) (tptp.fib_sorted (tptp.mycons X (tptp.mycons Y tptp.nil))))))
(assert (forall ((X Int) (Y Int) (Z Int) (R tptp.list)) (let ((_let_1 (tptp.mycons Y (tptp.mycons Z R)))) (=> (and (< X Y) (>= Z (+ X Y)) (tptp.fib_sorted _let_1)) (tptp.fib_sorted (tptp.mycons X _let_1))))))
(assert (not (tptp.fib_sorted (tptp.mycons 1 (tptp.mycons 2 (tptp.mycons 4 tptp.nil))))))
(set-info :filename tff0-arith)
(check-sat-assuming ( true ))
